Nuprl Lemma : R-sub-Rall
11,40
postcript
pdf
T
:Type,
L
:(
T
List),
R
:({
x
:
T
| (
x
L
)}
Realizer),
x
:
T
. (
x
L
)
R
(
x
)
x
L
.
R
(
x
)
latex
Definitions
x
L
.
P
(
x
)
,
S
T
,
,
P
&
Q
,
x
:
A
.
B
(
x
)
,
t
T
,
x
L
.
R
(
x
)
,
x
(
s
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
{
T
}
,
P
Q
,
P
Q
Lemmas
l
member
set
,
member
map
,
es
realizer
wf
,
map
wf
,
R-sub-Rlist
,
l
member
wf
,
list-subtype
origin
T:Type, L:(T List), R:({x:T| (x 
L)} 
Realizer), x:T. (x L) 
R(x) 
xL.R(x) T:Type, L:(T List), R:({x:T| (x L)} Realizer), x:T. (x L) R(x) xL.R(x) xL. P(x) T
x:A. B(x) TxL.R(x) Qx:A. B(x)
Q Q